Termination w.r.t. Q proof of /tmp/tmpCBgrL

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

Q3(y(x1)) → Y(q3(x1))
Y(q1(b(x1))) → Q2(y(y(x1)))
Q3(y(x1)) → Q3(x1)
A(q2(y(x1))) → A(y(x1))
Q0(a(x1)) → Q1(x1)
Q1(y(x1)) → Q1(x1)
Q0(y(x1)) → Q3(x1)
Q0(y(x1)) → Y(q3(x1))
A(q1(b(x1))) → A(y(x1))
A(q1(b(x1))) → Q2(a(y(x1)))
A(q2(y(x1))) → Q2(a(y(x1)))
Y(q2(y(x1))) → Q2(y(y(x1)))
Y(q2(a(x1))) → Y(a(x1))
Q1(a(x1)) → A(q1(x1))
A(q2(a(x1))) → Q2(a(a(x1)))
Y(q1(b(x1))) → Y(x1)
Y(q2(a(x1))) → Q2(y(a(x1)))
Y(q2(y(x1))) → Y(y(x1))
Y(q1(b(x1))) → Y(y(x1))
Q1(y(x1)) → Y(q1(x1))
A(q2(a(x1))) → A(a(x1))
A(q1(b(x1))) → Y(x1)
Q2(x(x1)) → Q0(x1)
Q1(a(x1)) → Q1(x1)

The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

Q3(y(x1)) → Y(q3(x1))
Y(q1(b(x1))) → Q2(y(y(x1)))
Q3(y(x1)) → Q3(x1)
A(q2(y(x1))) → A(y(x1))
Q0(a(x1)) → Q1(x1)
Q1(y(x1)) → Q1(x1)
Q0(y(x1)) → Q3(x1)
Q0(y(x1)) → Y(q3(x1))
A(q1(b(x1))) → A(y(x1))
A(q1(b(x1))) → Q2(a(y(x1)))
A(q2(y(x1))) → Q2(a(y(x1)))
Y(q2(y(x1))) → Q2(y(y(x1)))
Y(q2(a(x1))) → Y(a(x1))
Q1(a(x1)) → A(q1(x1))
A(q2(a(x1))) → Q2(a(a(x1)))
Y(q1(b(x1))) → Y(x1)
Y(q2(a(x1))) → Q2(y(a(x1)))
Y(q2(y(x1))) → Y(y(x1))
Y(q1(b(x1))) → Y(y(x1))
Q1(y(x1)) → Y(q1(x1))
A(q2(a(x1))) → A(a(x1))
A(q1(b(x1))) → Y(x1)
Q2(x(x1)) → Q0(x1)
Q1(a(x1)) → Q1(x1)

The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

Q0(a(x1)) → Q1(x1)
Q0(y(x1)) → Q3(x1)
Q0(y(x1)) → Y(q3(x1))
Q1(a(x1)) → A(q1(x1))
Q1(y(x1)) → Y(q1(x1))
Q2(x(x1)) → Q0(x1)

The remaining pairs can at least be oriented weakly.

Q3(y(x1)) → Y(q3(x1))
Y(q1(b(x1))) → Q2(y(y(x1)))
Q3(y(x1)) → Q3(x1)
A(q2(y(x1))) → A(y(x1))
Q1(y(x1)) → Q1(x1)
A(q1(b(x1))) → A(y(x1))
A(q1(b(x1))) → Q2(a(y(x1)))
A(q2(y(x1))) → Q2(a(y(x1)))
Y(q2(y(x1))) → Q2(y(y(x1)))
Y(q2(a(x1))) → Y(a(x1))
A(q2(a(x1))) → Q2(a(a(x1)))
Y(q1(b(x1))) → Y(x1)
Y(q2(a(x1))) → Q2(y(a(x1)))
Y(q2(y(x1))) → Y(y(x1))
Y(q1(b(x1))) → Y(y(x1))
A(q2(a(x1))) → A(a(x1))
A(q1(b(x1))) → Y(x1)
Q1(a(x1)) → Q1(x1)

Used ordering: Polynomial interpretation [25,35]:

POL(Q1(x₁)) = 1/2
POL(y(x₁)) = 0
POL(x(x₁)) = 4 + x_1
POL(q0(x₁)) = 4
POL(bl(x₁)) = 0
POL(q2(x₁)) = (4)x_1
POL(b(x₁)) = 0
POL(Q2(x₁)) = (4)x_1
POL(Q0(x₁)) = 2
POL(q3(x₁)) = 0
POL(q1(x₁)) = 0
POL(Q3(x₁)) = 0
POL(a(x₁)) = 0
POL(Y(x₁)) = 0
POL(q4(x₁)) = 0
POL(A(x₁)) = 0

The value of delta used in the strict ordering is 1/2.
The following usable rules [17] were oriented:

q0(a(x1)) → x(q1(x1))
q1(y(x1)) → y(q1(x1))
q1(a(x1)) → a(q1(x1))
a(q2(a(x1))) → q2(a(a(x1)))
a(q1(b(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q3(y(x1)) → y(q3(x1))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

Q3(y(x1)) → Y(q3(x1))
Y(q1(b(x1))) → Q2(y(y(x1)))
Q3(y(x1)) → Q3(x1)
A(q2(y(x1))) → A(y(x1))
Q1(y(x1)) → Q1(x1)
A(q1(b(x1))) → A(y(x1))
A(q1(b(x1))) → Q2(a(y(x1)))
A(q2(y(x1))) → Q2(a(y(x1)))
Y(q2(y(x1))) → Q2(y(y(x1)))
Y(q2(a(x1))) → Y(a(x1))
A(q2(a(x1))) → Q2(a(a(x1)))
Y(q1(b(x1))) → Y(x1)
Y(q2(a(x1))) → Q2(y(a(x1)))
A(q2(a(x1))) → A(a(x1))
Y(q1(b(x1))) → Y(y(x1))
Y(q2(y(x1))) → Y(y(x1))
A(q1(b(x1))) → Y(x1)
Q1(a(x1)) → Q1(x1)

The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 5 SCCs with 10 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

Y(q2(a(x1))) → Y(a(x1))
Y(q2(y(x1))) → Y(y(x1))

The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

Y(q2(a(x1))) → Y(a(x1))
Y(q2(y(x1))) → Y(y(x1))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(q1(x₁)) = (2)x_1
POL(y(x₁)) = (2)x_1
POL(x(x₁)) = 0
POL(q0(x₁)) = 0
POL(bl(x₁)) = 0
POL(a(x₁)) = x_1
POL(Y(x₁)) = (1/4)x_1
POL(q4(x₁)) = 0
POL(q2(x₁)) = 1 + (4)x_1
POL(b(x₁)) = 1/2 + (4)x_1
POL(q3(x₁)) = 0

The value of delta used in the strict ordering is 1/4.
The following usable rules [17] were oriented:

q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))
q0(a(x1)) → x(q1(x1))
q1(y(x1)) → y(q1(x1))
q1(a(x1)) → a(q1(x1))
a(q2(a(x1))) → q2(a(a(x1)))
a(q1(b(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
a(q2(y(x1))) → q2(a(y(x1)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

Q1(y(x1)) → Q1(x1)
Q1(a(x1)) → Q1(x1)

The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

Q1(y(x1)) → Q1(x1)
Q1(a(x1)) → Q1(x1)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(Q1(x₁)) = (4)x_1
POL(y(x₁)) = 4 + (4)x_1
POL(a(x₁)) = 1 + x_1

The value of delta used in the strict ordering is 4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

A(q2(y(x1))) → A(y(x1))
A(q2(a(x1))) → A(a(x1))

The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

A(q2(y(x1))) → A(y(x1))
A(q2(a(x1))) → A(a(x1))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(q1(x₁)) = (4)x_1
POL(y(x₁)) = (4)x_1
POL(x(x₁)) = 0
POL(q0(x₁)) = (4)x_1
POL(bl(x₁)) = 0
POL(a(x₁)) = (4)x_1
POL(q4(x₁)) = 0
POL(A(x₁)) = (1/4)x_1
POL(q2(x₁)) = 1/4 + x_1
POL(b(x₁)) = 1/4 + (4)x_1
POL(q3(x₁)) = 0

The value of delta used in the strict ordering is 1/16.
The following usable rules [17] were oriented:

q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))
q0(a(x1)) → x(q1(x1))
q1(y(x1)) → y(q1(x1))
q1(a(x1)) → a(q1(x1))
a(q2(a(x1))) → q2(a(a(x1)))
a(q1(b(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
a(q2(y(x1))) → q2(a(y(x1)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

              ↳ QDP

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

Y(q1(b(x1))) → Y(x1)

The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

Y(q1(b(x1))) → Y(x1)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(q1(x₁)) = 4 + (1/4)x_1
POL(Y(x₁)) = x_1
POL(b(x₁)) = (4)x_1

The value of delta used in the strict ordering is 4.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

Q3(y(x1)) → Q3(x1)

The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

Q3(y(x1)) → Q3(x1)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(y(x₁)) = 1/4 + (2)x_1
POL(Q3(x₁)) = (1/4)x_1

The value of delta used in the strict ordering is 1/16.
The following usable rules [17] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ QDPOrderProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

q0(a(x1)) → x(q1(x1))
q1(a(x1)) → a(q1(x1))
q1(y(x1)) → y(q1(x1))
a(q1(b(x1))) → q2(a(y(x1)))
a(q2(a(x1))) → q2(a(a(x1)))
a(q2(y(x1))) → q2(a(y(x1)))
y(q1(b(x1))) → q2(y(y(x1)))
y(q2(a(x1))) → q2(y(a(x1)))
y(q2(y(x1))) → q2(y(y(x1)))
q2(x(x1)) → x(q0(x1))
q0(y(x1)) → y(q3(x1))
q3(y(x1)) → y(q3(x1))
q3(bl(x1)) → bl(q4(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.